| Definitions |  T, es-state-when(es; e),  x:A. B(x), A c B, locl(a) sends [tg,f{A  T}(x)] on link l once, usends1-p-realizable, top, normal-type{i:l}(T), Rplus-right(x1), Rplus-left(x1), if b then t else f fi , Rplus?(x1), True, Y, reduce(f; k; as), Rlist(L), tt,  b, ff, implies-es-real, once-realizable, es-realizer(p), t.2, t.1, P Q, send_onceR{$done:ut2, $tg:ut2, $b:ut2, $done1:ut2}(T; A; f; l), Id,   x. t(x), prop{i:l}, t  T, mkid{$x:ut2}, P   Q,  x:A. B(x), e@i.P(e), alle-at(es; i; e.P(e)), usends1-p(es;ds;k;T;l;tg;B;f), @i locl(a) occurs once, decl-state(ds), Unit, False, guard(T), R-realizes{i:l}(R; es.P(es)), es-real{i:l}(es.P(es)), es_realizer{i:l}, x(s), Rrframe(loc; x; L), Rbframe(loc; k; L), Raframe(loc; k; L), Rsframe(lnk; tag; L), Rnone, Rplus(left; right), Rsends(ds; knd; T; l; dt; g), Rframe(loc; T; x; L), Reffect(loc; ds; knd; T; x; f), Rinit(loc; T; x; v), Rpre(loc; ds; a; p; P),  |
| Lemmas | es-isrcv wf, es-loc wf, es-E wf, es-vartype wf, es-kind-rcv, es-sender wf, es-when wf, es-val wf, rcv wf, es-kind wf, fpf-cap-single1, R-sub-plus-right3, subtype rel self, eqof eq btrue, id-deq wf, fpf-cap-single, fpf-single wf3, p-outcome wf, locl wf, usends1-p wf, normal-ds wf, tagof wf, lnk wf, ldst wf, isrcv wf, assert wf, unit-fps wf, natural number wf p-outcome, normal-ds-single, R-sub-plus-left, bool wf, finite-prob-space wf, decl-type wf, decl-state wf, fpf wf, Knd wf, rationals wf, unit wf, es realizer wf, false wf, true wf, R-sub-implies, lsrc wf, once-p wf, es-real wf, Id wf, IdLnk wf, normal-type wf, R-consistent wf, event system wf, send-once-p wf, implies-es-real, send onceR feasible, send onceR wf |
